Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar14/variousSLASH14.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

-¹₂(I₁(x), I₁(y)) -> O¹₁(-₂(x, y))
SIZE₁(N₃(x, l, r)) -> +¹₂(Size₁(l), Size₁(r))
+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
BS¹₁(N₃(x, l, r)) -> AND₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x))
BS¹₁(N₃(x, l, r)) -> MAX₁(l)
WB¹₁(N₃(x, l, r)) -> GE₂(Size₁(l), Size₁(r))
GE₂(0, O₁(x)) -> GE₂(0, x)
SIZE₁(N₃(x, l, r)) -> SIZE₁(l)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
WB¹₁(N₃(x, l, r)) -> AND₂(WB₁(l), WB₁(r))
GE₂(I₁(x), I₁(y)) -> GE₂(x, y)
LOG'₁(O₁(x)) -> +¹₂(Log'₁(x), I₁(0))
GE₂(I₁(x), O₁(y)) -> GE₂(x, y)
GE₂(O₁(x), I₁(y)) -> GE₂(y, x)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
WB¹₁(N₃(x, l, r)) -> SIZE₁(l)
WB¹₁(N₃(x, l, r)) -> WB¹₁(r)
-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
LOG'₁(O₁(x)) -> LOG'₁(x)
-¹₂(I₁(x), O₁(y)) -> -¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> O¹₁(+₂(+₂(x, y), I₁(0)))
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), O₁(y)) -> -¹₂(x, y)
SIZE₁(N₃(x, l, r)) -> +¹₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB¹₁(N₃(x, l, r)) -> AND₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))
BS¹₁(N₃(x, l, r)) -> BS¹₁(l)
WB¹₁(N₃(x, l, r)) -> -¹₂(Size₁(r), Size₁(l))
WB¹₁(N₃(x, l, r)) -> -¹₂(Size₁(l), Size₁(r))
BS¹₁(N₃(x, l, r)) -> GE₂(Min₁(r), x)
SIZE₁(N₃(x, l, r)) -> SIZE₁(r)
LOG'₁(I₁(x)) -> +¹₂(Log'₁(x), I₁(0))
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))
WB¹₁(N₃(x, l, r)) -> IF₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l))))
GE₂(O₁(x), I₁(y)) -> NOT₁(ge₂(y, x))
WB¹₁(N₃(x, l, r)) -> GE₂(I₁(0), -₂(Size₁(r), Size₁(l)))
WB¹₁(N₃(x, l, r)) -> GE₂(I₁(0), -₂(Size₁(l), Size₁(r)))
LOG'₁(O₁(x)) -> GE₂(x, I₁(0))
LOG₁(x) -> -¹₂(Log'₁(x), I₁(0))
BS¹₁(N₃(x, l, r)) -> BS¹₁(r)
LOG₁(x) -> LOG'₁(x)
BS¹₁(N₃(x, l, r)) -> AND₂(BS₁(l), BS₁(r))
BS¹₁(N₃(x, l, r)) -> AND₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
+¹₂(O₁(x), O₁(y)) -> O¹₁(+₂(x, y))
BS¹₁(N₃(x, l, r)) -> MIN₁(r)
GE₂(O₁(x), O₁(y)) -> GE₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)
WB¹₁(N₃(x, l, r)) -> WB¹₁(l)
WB¹₁(N₃(x, l, r)) -> SIZE₁(r)
BS¹₁(N₃(x, l, r)) -> GE₂(x, Max₁(l))
LOG'₁(O₁(x)) -> IF₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
-¹₂(O₁(x), O₁(y)) -> O¹₁(-₂(x, y))
MAX₁(N₃(x, l, r)) -> MAX₁(r)
LOG'₁(I₁(x)) -> LOG'₁(x)
MIN₁(N₃(x, l, r)) -> MIN₁(l)
+¹₂(O₁(x), O₁(y)) -> +¹₂(x, y)

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

-¹₂(I₁(x), I₁(y)) -> O¹₁(-₂(x, y))
SIZE₁(N₃(x, l, r)) -> +¹₂(Size₁(l), Size₁(r))
+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
BS¹₁(N₃(x, l, r)) -> AND₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x))
BS¹₁(N₃(x, l, r)) -> MAX₁(l)
WB¹₁(N₃(x, l, r)) -> GE₂(Size₁(l), Size₁(r))
GE₂(0, O₁(x)) -> GE₂(0, x)
SIZE₁(N₃(x, l, r)) -> SIZE₁(l)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
WB¹₁(N₃(x, l, r)) -> AND₂(WB₁(l), WB₁(r))
GE₂(I₁(x), I₁(y)) -> GE₂(x, y)
LOG'₁(O₁(x)) -> +¹₂(Log'₁(x), I₁(0))
GE₂(I₁(x), O₁(y)) -> GE₂(x, y)
GE₂(O₁(x), I₁(y)) -> GE₂(y, x)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
WB¹₁(N₃(x, l, r)) -> SIZE₁(l)
WB¹₁(N₃(x, l, r)) -> WB¹₁(r)
-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
LOG'₁(O₁(x)) -> LOG'₁(x)
-¹₂(I₁(x), O₁(y)) -> -¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> O¹₁(+₂(+₂(x, y), I₁(0)))
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), O₁(y)) -> -¹₂(x, y)
SIZE₁(N₃(x, l, r)) -> +¹₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB¹₁(N₃(x, l, r)) -> AND₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))
BS¹₁(N₃(x, l, r)) -> BS¹₁(l)
WB¹₁(N₃(x, l, r)) -> -¹₂(Size₁(r), Size₁(l))
WB¹₁(N₃(x, l, r)) -> -¹₂(Size₁(l), Size₁(r))
BS¹₁(N₃(x, l, r)) -> GE₂(Min₁(r), x)
SIZE₁(N₃(x, l, r)) -> SIZE₁(r)
LOG'₁(I₁(x)) -> +¹₂(Log'₁(x), I₁(0))
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))
WB¹₁(N₃(x, l, r)) -> IF₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l))))
GE₂(O₁(x), I₁(y)) -> NOT₁(ge₂(y, x))
WB¹₁(N₃(x, l, r)) -> GE₂(I₁(0), -₂(Size₁(r), Size₁(l)))
WB¹₁(N₃(x, l, r)) -> GE₂(I₁(0), -₂(Size₁(l), Size₁(r)))
LOG'₁(O₁(x)) -> GE₂(x, I₁(0))
LOG₁(x) -> -¹₂(Log'₁(x), I₁(0))
BS¹₁(N₃(x, l, r)) -> BS¹₁(r)
LOG₁(x) -> LOG'₁(x)
BS¹₁(N₃(x, l, r)) -> AND₂(BS₁(l), BS₁(r))
BS¹₁(N₃(x, l, r)) -> AND₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
+¹₂(O₁(x), O₁(y)) -> O¹₁(+₂(x, y))
BS¹₁(N₃(x, l, r)) -> MIN₁(r)
GE₂(O₁(x), O₁(y)) -> GE₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)
WB¹₁(N₃(x, l, r)) -> WB¹₁(l)
WB¹₁(N₃(x, l, r)) -> SIZE₁(r)
BS¹₁(N₃(x, l, r)) -> GE₂(x, Max₁(l))
LOG'₁(O₁(x)) -> IF₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
-¹₂(O₁(x), O₁(y)) -> O¹₁(-₂(x, y))
MAX₁(N₃(x, l, r)) -> MAX₁(r)
LOG'₁(I₁(x)) -> LOG'₁(x)
MIN₁(N₃(x, l, r)) -> MIN₁(l)
+¹₂(O₁(x), O₁(y)) -> +¹₂(x, y)

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 5 SCCs with 38 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(0, O₁(x)) -> GE₂(0, x)

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

GE₂(0, O₁(x)) -> GE₂(0, x)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
GE₂(x1, x2) = GE₁(x2)
0 = 0
O₁(x1) = O₁(x1)

Lexicographic Path Order [19].
Precedence:

[0, O_1] > GE₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(I₁(x), I₁(y)) -> GE₂(x, y)
GE₂(I₁(x), O₁(y)) -> GE₂(x, y)
GE₂(O₁(x), I₁(y)) -> GE₂(y, x)
GE₂(O₁(x), O₁(y)) -> GE₂(x, y)

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(I₁(x), O₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), O₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

-¹₂(I₁(x), O₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), O₁(y)) -> -¹₂(x, y)

The remaining pairs can at least by weakly be oriented.

-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

Used ordering: Combined order from the following AFS and order.
-¹₂(x1, x2) = -¹₁(x2)
I₁(x1) = x1
O₁(x1) = O₁(x1)
-₂(x1, x2) = -
1 = 1
0 = 0

Lexicographic Path Order [19].
Precedence:

[-^1₁, -] > 0 > [O₁, 1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)

The remaining pairs can at least by weakly be oriented.

-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

Used ordering: Combined order from the following AFS and order.
-¹₂(x1, x2) = -¹₁(x2)
I₁(x1) = I₁(x1)
O₁(x1) = O
-₂(x1, x2) = -₁(x2)
1 = 1
0 = 0

Lexicographic Path Order [19].
Precedence:

-^1₁ > I₁ > -₁ > [O, 1]
0 > [O, 1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
-¹₂(x1, x2) = x1
O₁(x1) = O₁(x1)
I₁(x1) = I₁(x1)
-₂(x1, x2) = x1
1 = 1
0 = 0

Lexicographic Path Order [19].
Precedence:

[O₁, I_1] > 0
1 > 0

The following usable rules [14] were oriented:

-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
O₁(0) -> 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(I₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(O₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

+¹₂(I₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(O₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

The remaining pairs can at least by weakly be oriented.

+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)

Used ordering: Combined order from the following AFS and order.
+¹₂(x1, x2) = +¹₁(x2)
I₁(x1) = x1
O₁(x1) = O₁(x1)
+₂(x1, x2) = +₂(x1, x2)
0 = 0

Lexicographic Path Order [19].
Precedence:

+^1₁ > +₂ > 0
O₁ > +₂ > 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)

The remaining pairs can at least by weakly be oriented.

+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))

Used ordering: Combined order from the following AFS and order.
+¹₂(x1, x2) = x2
O₁(x1) = O₁(x1)
I₁(x1) = I₁(x1)
+₂(x1, x2) = +₁(x2)
0 = 0

Lexicographic Path Order [19].
Precedence:

[I₁, +_1] > O₁ > 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

LOG'₁(O₁(x)) -> LOG'₁(x)
LOG'₁(I₁(x)) -> LOG'₁(x)

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

LOG'₁(I₁(x)) -> LOG'₁(x)

The remaining pairs can at least by weakly be oriented.

LOG'₁(O₁(x)) -> LOG'₁(x)

Used ordering: Combined order from the following AFS and order.
LOG'₁(x1) = LOG'₁(x1)
O₁(x1) = x1
I₁(x1) = I₁(x1)

Lexicographic Path Order [19].
Precedence:

trivial

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

LOG'₁(O₁(x)) -> LOG'₁(x)

The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

LOG'₁(O₁(x)) -> LOG'₁(x)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
LOG'₁(x1) = LOG'₁(x1)
O₁(x1) = O₁(x1)

Lexicographic Path Order [19].
Precedence:

O₁ > LOG'₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

O₁(0) -> 0
+₂(0, x) -> x
+₂(x, 0) -> x
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, 0) -> x
-₂(0, x) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))
not₁(true) -> false
not₁(false) -> true
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(O₁(x), O₁(y)) -> ge₂(x, y)
ge₂(O₁(x), I₁(y)) -> not₁(ge₂(y, x))
ge₂(I₁(x), O₁(y)) -> ge₂(x, y)
ge₂(I₁(x), I₁(y)) -> ge₂(x, y)
ge₂(x, 0) -> true
ge₂(0, O₁(x)) -> ge₂(0, x)
ge₂(0, I₁(x)) -> false
Log'₁(0) -> 0
Log'₁(I₁(x)) -> +₂(Log'₁(x), I₁(0))
Log'₁(O₁(x)) -> if₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
Log₁(x) -> -₂(Log'₁(x), I₁(0))
Val₁(L₁(x)) -> x
Val₁(N₃(x, l, r)) -> x
Min₁(L₁(x)) -> x
Min₁(N₃(x, l, r)) -> Min₁(l)
Max₁(L₁(x)) -> x
Max₁(N₃(x, l, r)) -> Max₁(r)
BS₁(L₁(x)) -> true
BS₁(N₃(x, l, r)) -> and₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
Size₁(L₁(x)) -> I₁(0)
Size₁(N₃(x, l, r)) -> +₂(+₂(Size₁(l), Size₁(r)), I₁(1))
WB₁(L₁(x)) -> true
WB₁(N₃(x, l, r)) -> and₂(if₃(ge₂(Size₁(l), Size₁(r)), ge₂(I₁(0), -₂(Size₁(l), Size₁(r))), ge₂(I₁(0), -₂(Size₁(r), Size₁(l)))), and₂(WB₁(l), WB₁(r)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.